\section{Alternative Passivation}
\newcommand{\loc}[2]{#1[#2]}
Here we introduce a core higher-order language with structured localities and forms of strong mobility, which features the same limitation in forwarding as \hof.
The objective is to show that with these additions, one recovers full Turing completeness.

We use 
%$\gamma$ for a possibly empty sequence of names, and
$\delta$ for a non-empty sequence of names. 
The concatenation of the two sequences of names $\delta_{1}$ and $\delta_{2}$ is written $\delta_{1}\delta_{2}$.
The syntax of processes is as follows:

\[P :: = \delta(x). P \midd \overline{\delta}(x). P \midd \Ho{\delta}{P}\midd \loc{\delta}{P} \midd P \parallel P \midd x \midd \nil \]  

with the following requirement: the $P$ in 
the output prefix $\Ho{\delta}{P}$ and in the locality $\loc{\delta}{P}$ adheres to the forwarding limitation of \hof.
The non-standard prefix $\overline{\delta}(x)$ represents ``take from $\delta$'', as a form of strong process mobility. 
This is in contrast with the usual prefix $\delta(x)$, which represents ``receive on $\delta$''.
The LTS, given in Figure \ref{fig:lts-chomer},  has five kinds of actions: $\tau$, $\overline{\delta}(x)$, $\delta(x)$, $\Ho{\delta}{P}$, and $\loc{\delta}{P}$.

\begin{figure}[h]
$$\mathrm{\textsc{Inp}}~~~{\delta(x). P} \arr{\delta(x)  }  {P } \quad \mathrm{\textsc{Take}}~~~{\overline{\delta}(x). P} \arr{\overline{\delta}(x)  }  {P } \quad \mathrm{\textsc{Loc}}~~~ {\loc{\delta}{P}} \arr{\loc{\delta}{P}} {\nil} \quad \mathrm{\textsc{Out}}~~~{\Ho{\delta}{P}} \arr{\Ho{\delta}{P}} {\nil}  $$
$$
\rightinfer	[\textsc{Act1}]
			{P_1 \parallel P_2 \arr\alpha P'_1 \parallel P_2}
			{P_1 \arr\alpha P_1'  \andalso \bv \alpha \cap \fv{ P_2} = \emptyset}
\qquad
\rightinfer	[\textsc{Tau1}]
			{P_1 \parallel P_2 \arr\tau  P'_1 \parallel P'_2 \sub{P}{x}}
			{P_1 \arr{\overline{\delta}{\langle P \rangle}} P_1' \andalso P_2 \arr{\delta(x)} P'_2}
$$
$$		
\rightinfer	[\textsc{Tau3}]
			{P_1 \parallel P_2 \arr\tau  P'_1 \parallel P'_2 \sub{P}{x}}
			{P_1 \arr{\loc{\delta}{P}} P_1' \andalso P_2 \arr{\overline{\delta}(x)} P'_2}
			\qquad	
\rightinfer	[\textsc{Nest}]
			{\loc{\delta}{P} \arr{\delta\cdot\alpha} \loc{\delta}{P'}}
			{P \arr{\alpha} P'}
$$
\caption{An LTS for a core Homer, with forwarding as in \hof.
Rules \textsc{Act2}, \textsc{Tau2}, and \textsc{Tau4}, the symmetric counterparts of 
\textsc{Act1}, \textsc{Tau1}, and \textsc{Tau3}, have been omitted.} \label{fig:lts-chomer}
\end{figure}

The semantics exploits an operation on actions and sequences of names.
We define $\delta\cdot\alpha$ as: $\delta\cdot\tau = \tau$, $\delta\cdot\delta'(x) = \delta\delta'(x)$, 
$\delta\cdot\loc{\delta'}{P} = \loc{\delta\delta'}{P}$, and undefined for take and send.

We can encode Minsky machines in this ``core Homer'':

\begin{table}[t] 
\centering  
{%\small 
\begin{tabular}{l}   
\(  
\mathrm{\textsc{Register}}~r_k \qquad
\encp{r_k = n}{\mms}   =  \loc{r_k}{\encn{n}{k}} 
\) \\ %where

\quad where \\

\quad \quad \quad  \(  
\encn{n}{k}=\left\{  
\begin{array}{ll}  
 \overline{s \cdot z_k}(x).\overline{s \cdot a_z}  & \textrm{if } n= 0 \\  
 \overline{d\cdot u_k}(x).(\overline{d \cdot a_1} \parallel a_2.\encn{n-1}{k}) ~~& \textrm{if } n> 0 .  
\end{array}\right.  
\)
 
\\ \\ 

\(
\begin{array}{lll}   
\multicolumn{3}{l}{\mathrm{\textsc{Instructions}}~(i:I_i)}\\  
\encp{(i: \mathtt{INC}(r_k))}{\mms}&  = &  !\,p_i.( r_k(x).(\Ho{r_{k}\cdot c_k}{x} \parallel \loc{r_k}{c_k(y).(\loc{a_p}{-} \parallel \overline{d\cdot u_k}(x).(\overline{d \cdot a_1} \parallel a_2.y)) } \\
& & \qquad \qquad \qquad \quad \parallel  \overline{r_{k}\cdot a_p}(x).\overline{p_{i+1}}))\\
\encp{(i: \mathtt{DECJ}(r_k,s))}{\mms}&  = & !\,{p_i}.\overline{r_{k}}(x).\loc{r_{k}}{\,  x  \parallel \overline{d \cdot m}(x).x \parallel \overline{s \cdot m}(x).x \parallel   \\
& &  \qquad \qquad \qquad \parallel \loc{d}{\loc{u_k}{-} \parallel a_1.\loc{m}{\overline{s}(x).\overline{d}(x).(\overline{a_2} \parallel \loc{a_{d}^{i}}{-})}} \\
& &  \qquad \qquad \qquad \parallel \loc{s}{\loc{z_k}{-} \parallel a_z.\loc{m}{\overline{d}(x).\overline{s}(x).\overline{s \cdot z_k}(x).\overline{s \cdot a_z} \parallel \loc{a_{s}^{i}}{-}}} \, }  \\ 
& & \parallel !\, \overline{r_{k} \cdot a_{d}^{i}}(x).\overline{p_{i+1}} \parallel  !\, \overline{r_{k} \cdot a_{s}^{i}}(x).\overline{p_{s}}
\end{array}   
\) \\ \\

\end{tabular}
}  
\caption{Encoding of Minsky machines into core Homer. There is garbage that can be collected.}  
\label{t:encod-chomer}  
%\vspace{-5mm}
\end{table}

